Nicolaas de Bruijn, Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, Indagationes Mathematicae (Proceedings) 75 5 (1972) 381-392 [doi:10.1016/1385-7258(72)90034-0, pdf]